package com.starview.star.compiler.type;

import com.starview.platform.data.IArray;
import com.starview.platform.data.IValue;
import com.starview.platform.data.type.*;
import com.starview.star.compiler.CompilerUtils;
import com.starview.star.compiler.ErrorReport;
import com.starview.star.compiler.ast.*;
import com.starview.star.compiler.cafe.CafeSyntax;
import com.starview.star.compiler.canonical.Variable;
import com.starview.star.compiler.standard.StandardNames;
import com.starview.star.compiler.transform.OverLoader;
import com.starview.star.compiler.util.*;
import com.starview.star.operators.assignment.runtime.RefCell.Cell;

import java.util.*;
import java.util.Map.Entry;

public class TypeParser{
  public static IAlgebraicType parseTypeDefinition(IAbstract stmt, Map<String, Pair<IAbstract, IType>> defaults,
                                                   Map<String, IAbstract> integrity, Dictionary dict,
                                                   Dictionary outer, ErrorReport errors, boolean suppress){
    LayeredMap<String, TypeVar> typeVars = new LayeredHash<>();
    Dictionary tmpCxt = dict.fork();
    Location loc = stmt.getLoc();

    TypeNameHandler varHandler = new RegularTypeName(tmpCxt, typeVars, AccessMode.readOnly, suppress, errors);
    TypeNameHandler defHandler = new DefiningTypeName(tmpCxt, typeVars, AccessMode.readOnly);

    IType thisType = typeHead(CompilerUtils.typeDefnType(stmt), tmpCxt, errors, defHandler);

    IAbstract constructors = CompilerUtils.typeDefnConstructors(stmt);

    if (Abstract.isBinary(constructors, StandardNames.WHERE)) {
      parseConstraints(Abstract.binaryRhs(constructors), dict, errors, varHandler);
      constructors = Abstract.binaryLhs(constructors);
    }

    ITypeDescription desc = dict.getTypeDescription(thisType.typeLabel());

    if (!(desc instanceof IAlgebraicType)) {
      desc = new TypeDescription(loc, Refresher.generalize(thisType, typeVars));
      dict.defineType(desc);
    }

    IAlgebraicType algebraicType = (IAlgebraicType) desc;
    parseAlgebraicConstructors(constructors, thisType, algebraicType, tmpCxt, outer, errors, typeVars);
    parseDefaults(constructors, thisType, tmpCxt, algebraicType, defaults, integrity, errors);

    return algebraicType;
  }

  public static IType parseType(IAbstract tp, Dictionary cxt, ErrorReport errors, AccessMode access){
    Map<String, TypeVar> typeVars = new HashMap<>();
    TypeNameHandler varHandler = new RegularTypeName(cxt, typeVars, access, false, errors);
    return parseType(tp, cxt, errors, varHandler);
  }

  public static IType parseType(IAbstract tp, Dictionary cxt, ErrorReport errors, AccessMode access, boolean suppress){
    final LayeredMap<String, TypeVar> typeVars = new LayeredHash<>();
    TypeNameHandler varHandler = new RegularTypeName(cxt, typeVars, access, suppress, errors);
    return parseType(tp, cxt, errors, varHandler);
  }

  public static IType parseType(IAbstract tp, LayeredMap<String, TypeVar> typeVars, Dictionary dict,
                                ErrorReport errors, AccessMode access){
    TypeNameHandler varHandler = new RegularTypeName(dict, typeVars, access, false, errors);
    return parseType(tp, dict, errors, varHandler);
  }

  public static class RegularTypeName implements TypeNameHandler{
    private final Dictionary dict;
    private final Map<String, TypeVar> typeVars;
    private final AccessMode access;
    private final boolean suppress;
    private final ErrorReport errors;

    public RegularTypeName(Dictionary dict, Map<String, TypeVar> typeVars, AccessMode access, boolean supress,
                           ErrorReport errors){
      this.dict = dict;
      this.typeVars = typeVars;
      this.access = access;
      this.suppress = supress;
      this.errors = errors;
    }

    @Override
    public IType typeByName(String name, Location loc){
      if (typeVars.containsKey(name))
        return typeVars.get(name);
      else {
        ITypeDescription desc = dict.getTypeDescription(name);

        if (desc == null) {
          if (!TypeUtils.isStdType(name) && !suppress)
            errors.reportError("type " + name + " not declared", loc);
          return new Type(name, Kind.unknown);
        }

        IType type = new Type(name, desc.kind());

        try {
          type = typeAlias(dict, type, loc);
        } catch (TypeConstraintException e) {
          errors.reportError(e.getMessage(), Location.merge(loc, e.getLocs()));
          return type;
        }
        return type;
      }
    }

    @Override
    public TypeVar newTypeVar(String name, Location loc){
      if (typeVars.containsKey(name))
        return typeVars.get(name);
      else {
        TypeVar v = new TypeVar(name, access);
        typeVars.put(name, v);
        return v;
      }
    }

    @Override
    public void addEntries(Map<String, TypeVar> sub){
      typeVars.putAll(sub);
    }

    @Override
    public void defineType(String name, TypeVar v){
      typeVars.put(name, v);
    }

    @Override
    public void removeEntries(Map<String, TypeVar> rem){
      for (Entry<String, TypeVar> e : rem.entrySet())
        typeVars.remove(e.getKey());
    }

    @Override
    public AccessMode access(){
      return access;
    }

    @Override
    public Map<String, TypeVar> typeVars(){
      return typeVars;
    }

    @Override
    public boolean suppressWarnings(){
      return suppress;
    }
  }

  public static class DefiningTypeName implements TypeNameHandler{
    private final Dictionary dict;
    private final Map<String, TypeVar> typeVars;
    private final AccessMode access;

    public DefiningTypeName(Dictionary dict, Map<String, TypeVar> typeVars, AccessMode access){
      this.dict = dict;
      this.typeVars = typeVars;
      this.access = access;
    }

    @Override
    public IType typeByName(String name, Location loc){
      if (typeVars.containsKey(name))
        return typeVars.get(name);
      else {
        ITypeDescription desc = dict.getTypeDescription(name);

        if (desc == null)
          return newTypeVar(name, loc);

        return new Type(name, Kind.unknown);
      }
    }

    @Override
    public TypeVar newTypeVar(String name, Location loc){
      if (typeVars.containsKey(name))
        return typeVars.get(name);
      else {
        TypeVar v = new TypeVar(name, access);
        typeVars.put(name, v);
        return v;
      }
    }

    @Override
    public void addEntries(Map<String, TypeVar> sub){
      typeVars.putAll(sub);
    }

    @Override
    public void defineType(String name, TypeVar v){
      typeVars.put(name, v);
    }

    @Override
    public void removeEntries(Map<String, TypeVar> rem){
      for (Entry<String, TypeVar> e : rem.entrySet())
        typeVars.remove(e.getKey());
    }

    @Override
    public AccessMode access(){
      return access;
    }

    @Override
    public Map<String, TypeVar> typeVars(){
      return typeVars;
    }

    @Override
    public boolean suppressWarnings(){
      return true;
    }
  }

  public static IType parseType(IAbstract tp, Dictionary dict, ErrorReport errors, TypeNameHandler varHandler){
    final Location loc = tp.getLoc();
    if (tp instanceof Name) {
      String tpName = ((Name) tp).getId();

      if (tpName.equals(StandardNames.BRACES))
        return new TypeInterfaceType();
      else
        return varHandler.typeByName(tpName, loc);
    } else if (CompilerUtils.isTypeVar(tp))
      return varHandler.newTypeVar(CompilerUtils.typeVarName(tp), loc);
    else if (CompilerUtils.isTypeFunVar(tp))
      return varHandler.newTypeVar(CompilerUtils.typeVarName(tp), loc);
    else if (CompilerUtils.isRef(tp)) {
      IAbstract ref = Abstract.deParen(CompilerUtils.referencedTerm(tp));

      IType refType = parseType(ref, dict, errors, varHandler);

      return TypeUtils.referenceType(refType);
    } else if (Abstract.isBinary(tp, StandardNames.OF)) {
      IAbstract con = Abstract.binaryLhs(tp);
      List<IType> typeArgList = parseArgTypes(Abstract.binaryRhs(tp), dict, errors, varHandler);

      IType tyCon = parseType(con, dict, errors, varHandler);

      tyCon = checkKind(tyCon, Kind.kind(typeArgList.size()), loc, errors);
      IType type = TypeUtils.typeExp(tyCon, typeArgList);

      try {
        type = typeAlias(dict, type, loc);
      } catch (TypeConstraintException e) {
        errors.reportError(e.getMessage(), Location.merge(loc, e.getLocs()));
      }

      return type;
    } else if (CompilerUtils.isUniversalType(tp)) {
      IAbstract tArg = CompilerUtils.universalTypeVars(tp);
      IAbstract bndArg = CompilerUtils.universalBoundType(tp);
      Map<String, TypeVar> bndTypes = parseQuantifiers(tArg, errors);

      varHandler.addEntries(bndTypes);

      IType boundType = parseType(bndArg, dict, errors, varHandler);

      varHandler.removeEntries(bndTypes);
      return UniversalType.univ(bndTypes.values(), boundType);
    } else if (CompilerUtils.isExistentialType(tp)) {
      IAbstract tArg = CompilerUtils.existentialTypeVars(tp);
      IAbstract bndArg = CompilerUtils.existentialBoundType(tp);
      Map<String, TypeVar> bndTypes = parseQuantifiers(tArg, errors);
      varHandler.addEntries(bndTypes);

      IType boundType = parseType(bndArg, dict, errors, varHandler);

      varHandler.removeEntries(bndTypes);
      return ExistentialType.exist(bndTypes.values(), boundType);
    } else if (Abstract.isBinary(tp, StandardNames.FUN_TYPE)) {
      IType argsType = parseFunArgType(Abstract.binaryLhs(tp), dict, errors, varHandler);

      IType resltType = parseType(Abstract.binaryRhs(tp), dict, errors, varHandler);

      return TypeUtils.funcType(argsType, resltType);
    } else if (Abstract.isBinary(tp, StandardNames.OVERLOADED_TYPE)) {
      IType conArgType = parseFunArgType(Abstract.binaryLhs(tp), dict, errors, varHandler);
      IType resType = parseType(Abstract.binaryRhs(tp), dict, errors, varHandler);

      return TypeUtils.overloadedType(conArgType, resType);
    } else if (Abstract.isRoundTerm(tp, StandardNames.ACTION_TYPE)) {
      List<IType> argTypes = new ArrayList<>();
      for (IValue tpArg : Abstract.getArgs(tp))
        argTypes.add(parseType((IAbstract) tpArg, dict, errors, varHandler));
      return TypeUtils.procedureType(argTypes);
    } else if (Abstract.isBinary(tp, StandardNames.PTN_TYPE)) {
      IType argsType = parseFunArgType(Abstract.binaryLhs(tp), dict, errors, varHandler);
      IType ptnType = parseType(Abstract.binaryRhs(tp), dict, errors, varHandler);
      return TypeUtils.patternType(argsType, ptnType);
    } else if (Abstract.isBinary(tp, StandardNames.CONSTRUCTOR_TYPE)) {
      IType argsType = parseFunArgType(Abstract.binaryLhs(tp), dict, errors, varHandler);
      IType resltType = parseType(Abstract.binaryRhs(tp), dict, errors, varHandler);

      return TypeUtils.constructorType(argsType, resltType);
    } else if (Abstract.isParenTerm(tp))
      return parseType(Abstract.deParen(tp), dict, errors, varHandler);
    else if (CompilerUtils.isFieldAccess(tp) && Abstract.isIdentifier(CompilerUtils.fieldRecord(tp))
            && Abstract.isIdentifier(CompilerUtils.fieldField(tp))) {
      String record = Abstract.getId(CompilerUtils.fieldRecord(tp));
      String field = Abstract.getId(CompilerUtils.fieldField(tp));

      // We need to handle this carefully because we would like to avoid unnecessary skolemization

      DictInfo info = dict.getVar(record);

      if (info instanceof VarInfo)
        return ((VarInfo) info).localType(loc, field, dict, errors);
      else {
        errors.reportError("type " + field + " from " + record + " is not valid here", loc);
        return new TypeVar();
      }
    } else if (Abstract.isBinary(tp, StandardNames.WHERE)) {
      IType type = parseType(Abstract.binaryLhs(tp), dict, errors, varHandler);
      parseConstraints(Abstract.binaryRhs(tp), dict, errors, varHandler);
      return type;
    } else if (Abstract.isTupleTerm(tp)) {
      IArray tpl = Abstract.tupleArgs(tp);
      IType elTypes[] = new IType[tpl.size()];
      for (int ix = 0; ix < elTypes.length; ix++)
        elTypes[ix] = parseType((IAbstract) tpl.getCell(ix), dict, errors, varHandler);
      return TypeUtils.tupleType(elTypes);
    } else if (CompilerUtils.isInterfaceType(tp))
      return parseInterfaceType(loc, CompilerUtils.interfaceTypeElements(tp), errors, dict, varHandler);
    else if (Abstract.isBinary(tp, StandardNames.DETERMINES)) {
      IType lhs = parseType(Abstract.binaryLhs(tp), dict, errors, varHandler);

      List<IType> detArgs = parseArgTypes(Abstract.binaryRhs(tp), dict, errors, varHandler);

      IType[] lArgs = TypeUtils.typeArgs(lhs);
      int lArity = lArgs.length;
      IType args[] = new IType[lArity + 1];
      System.arraycopy(lArgs, 0, args, 0, lArity);
      args[lArity] = TypeUtils.typeExp(StandardNames.DETERMINES, detArgs);
      return TypeUtils.typeExp(lhs.typeLabel(), args);
    } else {
      errors.reportError("cannot understand type expression: " + tp, loc);
      return new TypeVar();
    }
  }

  private static IType checkKind(IType type, Kind kind, Location loc, ErrorReport errors){
    type = TypeUtils.deRef(type);
    if (!kind.equals(Kind.unknown)) {
      if (type instanceof Type) {
        Type t = (Type) type;

        if (t.kind().equals(Kind.unknown))
          return new Type(t.typeLabel(), kind);
        else if (!t.kind().checkKind(kind))
          errors.reportError(StringUtils.msg("type ", type, " not consistent with ", kind), loc);
      } else if (type instanceof TypeVar)
        if (!((TypeVar) type).checkKind(kind))
          errors.reportError(StringUtils.msg("type ", type, " not consistent with ", kind), loc);
    }
    return type;
  }

  private static Map<String, TypeVar> parseQuantifiers(IAbstract tArg, ErrorReport errors){
    Map<String, TypeVar> bndTypes = new HashMap<>();
    for (IAbstract tA : CompilerUtils.unWrap(tArg, StandardNames.COMMA)) {
      if (CompilerUtils.isTypeVar(tA)) {
        String vrName = CompilerUtils.typeVarName(tA);
        TypeVar var = new TypeVar(vrName, vrName, AccessMode.readOnly);
        bndTypes.put(vrName, var);
      } else if (CompilerUtils.isTypeFunVar(tA)) {
        String vrName = CompilerUtils.typeFunVarName(tA);
        TypeVar var = TypeVar.var(vrName, 1, AccessMode.readOnly);
        bndTypes.put(vrName, var);
      } else if (Abstract.isIdentifier(tA)) {
        String vrName = Abstract.getId(tA);
        TypeVar var = new TypeVar(vrName, vrName, AccessMode.readOnly);
        bndTypes.put(vrName, var);
      } else
        errors.reportError("invalid bound type variable: " + tA, tA.getLoc());
    }
    return bndTypes;
  }

  private static IType parseFunArgType(IAbstract tp, Dictionary cxt, ErrorReport errors, TypeNameHandler varHandler){
    if (Abstract.isTupleTerm(tp)) {
      List<IType> argTypes = new ArrayList<>();

      for (IValue a : ((Apply) tp).getArgs())
        argTypes.add(parseType((IAbstract) a, cxt, errors, varHandler));

      return TypeUtils.tupleType(argTypes);
    } else if (CompilerUtils.isBlockTerm(tp))
      return parseType(tp, cxt, errors, varHandler);
    else {
      errors.reportError("expecting a tuple of arguments to function type, not " + tp, tp.getLoc());
      return TypeUtils.tupleType(parseType(tp, cxt, errors, varHandler));
    }
  }

  /**
   * Valid constraints include
   * <p/>
   * con over (t1,..,tn)
   * <p/>
   * {field has type tp; ... ; field has type tpn}
   * <p/>
   * %t depends on tp
   * <p/>
   * constraint 'n constraint
   *
   * @param varHandler callback to handle occurrences of names
   */
  private static void parseConstraints(IAbstract cons, final Dictionary cxt, final ErrorReport errors,
                                       TypeNameHandler varHandler){
    final Location loc = cons.getLoc();

    if (Abstract.isParenTerm(cons))
      parseConstraints(Abstract.deParen(cons), cxt, errors, varHandler);
    else if (Abstract.isBinary(cons, StandardNames.ALSO)) {
      parseConstraints(Abstract.binaryLhs(cons), cxt, errors, varHandler);
      parseConstraints(Abstract.binaryRhs(cons), cxt, errors, varHandler);
    } else if (Abstract.isBinary(cons, StandardNames.IMPLEMENTS)
            && (CompilerUtils.isTypeVar(Abstract.binaryLhs(cons)) || Abstract.isIdentifier(Abstract.binaryLhs(cons)))
            && CompilerUtils.isInterfaceType(Abstract.binaryRhs(cons))) {
      final TypeVar tVar = (TypeVar) parseType(Abstract.binaryLhs(cons), cxt, errors, varHandler);

      ITypeCollector hndlr = new ITypeCollector(){
        @Override
        public void fieldAnnotation(Location loc, String name, IType type){
          try {
            TypeUtils.addFieldConstraint(tVar, loc, name, type, cxt, true);
          } catch (TypeConstraintException e) {
            errors.reportError(StringUtils.msg("could not add constraint ", name, " has type ", type, "\nbecause ", e
                    .getWords()), Location.merge(loc, e.getLocs()));
          }
        }

        @Override
        public void kindAnnotation(Location loc, String name, IType type){
          try {
            TypeUtils.addTypeConstraint(tVar, loc, name, type, cxt, true);
          } catch (TypeConstraintException e) {
            errors.reportError(StringUtils.msg("could not add constraint ", name, " has kind ", type.kind(),
                    "\nbecause ", e.getWords()), Location.merge(loc, e.getLocs()));
          }
        }

        @Override
        public void completeInterface(Location loc){
        }
      };
      findMemberTypes(loc, CompilerUtils.interfaceTypeElements(Abstract.binaryRhs(cons)), hndlr, cxt, errors,
              varHandler);
    } else if (CompilerUtils.isKindAnnotation(cons)) {
      IType bndType = parseType(CompilerUtils.kindAnnotatedTerm(cons), cxt, errors, varHandler);
      if (bndType instanceof TypeVar) {
        TypeVar tv = (TypeVar) bndType;

        IAbstract tpSpec = CompilerUtils.kindAnnotation(cons);

        if (Abstract.isIdentifier(tpSpec, StandardNames.TYPE)) {
          tv.setConstraint(new HasKind(tv, Kind.type));
        } else if (Abstract.isBinary(tpSpec, StandardNames.OF)) {
          IAbstract kindArgs = Abstract.deParen(Abstract.binaryRhs(tpSpec));
          int arity = 0;
          if (Abstract.isIdentifier(kindArgs, StandardNames.TYPE))
            arity = 1;
          else if (Abstract.isTupleTerm(kindArgs))
            arity = Abstract.tupleArity(kindArgs);
          else
            errors.reportError(StringUtils.msg("invalid declaration of kind: ", tpSpec), loc);
          tv.setConstraint(new HasKind(tv, Kind.kind(arity)));
        } else
          errors.reportError(StringUtils.msg("invalid kind specification: ", tpSpec), loc);

        IAbstract constraint = CompilerUtils.kindAnnotatedConstraint(cons);
        if (constraint != null)
          parseConstraints(CompilerUtils.kindAnnotatedConstraint(cons), cxt, errors, varHandler);
      } else
        errors.reportError(StringUtils.msg("invalid kind specification: ", cons), loc);
    } else if (Abstract.isBinary(cons, StandardNames.INSTANCE_OF) && CompilerUtils.isTypeVar(Abstract.binaryLhs(cons)
    )) {
      final TypeVar var = (TypeVar) parseType(Abstract.binaryLhs(cons), cxt, errors, varHandler);

      IType general = parseType(Abstract.binaryRhs(cons), cxt, errors, varHandler);
      ITypeConstraint con = new InstanceOf(var, general);
      try {
        var.addConstraint(con, loc, cxt);
      } catch (TypeConstraintException e) {
        errors.reportError("could not add constraint " + cons + "\nbecause " + e.getMessage(), Location.merge(loc, e
                .getLocs()));
      }
    } else if (Abstract.isBinary(cons, StandardNames.OVER)) {
      IAbstract conTp = Abstract.binaryRhs(cons);
      String contractName = Abstract.getId(Abstract.binaryLhs(cons));
      TypeContract contract = cxt.getContract(contractName);
      if (contract == null && !varHandler.suppressWarnings())
        errors.reportError(StringUtils.msg("contract ", contractName, " is not known"), loc);
      if (Abstract.isBinary(conTp, StandardNames.DETERMINES)) {
        List<IType> argTypes = parseArgTypes(Abstract.binaryLhs(conTp), cxt, errors, varHandler);

        for (IType tp : argTypes)
          if (!TypeUtils.isTypeVar(tp))
            errors.reportError("type constraint must be over a type variable, not " + tp, Abstract.binaryLhs(conTp)
                    .getLoc());

        List<IType> depTypes = parseArgTypes(Abstract.binaryRhs(conTp), cxt, errors, varHandler);
        argTypes.add(TypeUtils.typeExp(StandardNames.DETERMINES, depTypes));

        TypeExp contractType = (TypeExp) TypeUtils.typeExp(contractName, argTypes);

        if (contract != null)
          try {
            Subsume.subsume(contractType, Freshen.freshenForUse(contract.getContractType().getType()), loc, cxt, true);
          } catch (TypeConstraintException e) {
            errors.reportError(StringUtils.msg("contract constraint ", cons, " not consistent with contract ",
                    contractName, "\nbecause ", e.getWords()), loc);
          }

        ITypeConstraint con = new ContractConstraint(contractType);

        for (IType tp : argTypes)
          if (TypeUtils.isTypeVar(tp))
            ((TypeVar) TypeUtils.deRef(tp)).setConstraint(con);
      } else {
        List<IType> argTypes = parseArgTypes(Abstract.binaryRhs(cons), cxt, errors, varHandler);
        TypeExp contractType = (TypeExp) TypeUtils.typeExp(contractName, argTypes);

        if (contract != null)
          try {
            Subsume.subsume(contractType, Freshen.freshenForUse(contract.getContractType().getType()), loc, cxt, true);
          } catch (TypeConstraintException e) {
            errors.reportError(StringUtils.msg("contract constraint ", cons, " not consistent with contract ",
                    contractName, "\nbecause ", e.getWords()), loc);
          }
        ITypeConstraint con = new ContractConstraint(contractType);

        for (IType tp : argTypes)
          if (TypeUtils.isTypeVar(tp))
            ((TypeVar) TypeUtils.deRef(tp)).setConstraint(con);
      }
    } else if (Abstract.isUnary(cons, StandardNames.TUPLE) && CompilerUtils.isTypeVar(Abstract.unaryArg(cons))) {

      final TypeVar tVar = (TypeVar) parseType(Abstract.unaryArg(cons), cxt, errors, varHandler);
      TupleConstraint con = new TupleConstraint(tVar);
      tVar.setConstraint(con);
    } else
      errors.reportError("not a valid type constraint: " + cons, loc);
  }

  public static TypeExp parseContractType(IAbstract tp, Dictionary cxt, ErrorReport errors, TypeNameHandler varHandler){
    if (Abstract.isBinary(tp, StandardNames.WHERE)) {
      TypeExp type = parseContractType(Abstract.binaryLhs(tp), cxt, errors, varHandler);
      parseConstraints(Abstract.binaryRhs(tp), cxt, errors, varHandler);
      return type;
    } else if (Abstract.isBinary(tp, StandardNames.OVER)) {
      IAbstract conTp = Abstract.binaryRhs(tp);
      if (Abstract.isBinary(conTp, StandardNames.DETERMINES)) {
        List<IType> argTypes = parseArgTypes(Abstract.binaryLhs(conTp), cxt, errors, varHandler);
        List<IType> depTypes = parseArgTypes(Abstract.binaryRhs(conTp), cxt, errors, varHandler);
        argTypes.add(TypeUtils.typeExp(StandardNames.DETERMINES, depTypes));
        return (TypeExp) TypeUtils.typeExp(Abstract.getId(Abstract.binaryLhs(tp)), argTypes);
      } else {
        List<IType> argTypes = parseArgTypes(Abstract.binaryRhs(tp), cxt, errors, varHandler);
        return (TypeExp) TypeUtils.typeExp(Abstract.getId(Abstract.binaryLhs(tp)), argTypes);
      }
    } else {
      errors.reportError("not a valid contract specification: " + tp, tp.getLoc());
      return (TypeExp) StandardTypes.voidType;
    }
  }

  public static IType parseContractImplType(IAbstract tp, Dictionary cxt, ErrorReport errors, boolean suppress,
                                            boolean isFallback){
    Dictionary dict = cxt.fork();
    TypeNameHandler varHandler = new RegularTypeName(dict, new HashMap<String, TypeVar>(), AccessMode.readOnly,
            suppress, errors);
    return parseContractImplType(tp, dict, varHandler, isFallback, errors);
  }

  private static IType parseContractImplType(IAbstract tp, Dictionary cxt, TypeNameHandler varHandler,
                                             boolean isFallback, ErrorReport errors){
    while (CompilerUtils.isUniversalType(tp)) {
      for (IAbstract tv : CompilerUtils.unWrap(CompilerUtils.universalTypeVars(tp), StandardNames.COMMA)) {
        if (CompilerUtils.isTypeVar(tv) || CompilerUtils.isTypeFunVar(tv))
          tv = CompilerUtils.typeVName(tv);
        varHandler.newTypeVar(Abstract.getId(tv), tv.getLoc());
      }
      tp = CompilerUtils.universalBoundType(tp);
    }
    if (Abstract.isBinary(tp, StandardNames.WHERE)) {
      IType type = parseContractImplType(Abstract.binaryLhs(tp), cxt, varHandler, isFallback, errors);
      parseConstraints(Abstract.binaryRhs(tp), cxt, errors, varHandler);
      return type;
    } else if (Abstract.isBinary(tp, StandardNames.OVER)
            && Abstract.isBinary(Abstract.binaryRhs(tp), StandardNames.DETERMINES)) {
      IAbstract implType = Abstract.binaryLhs(Abstract.binaryRhs(tp));
      List<IType> argTypes = parseArgTypes(implType, cxt, errors, varHandler);
      IType dependent = TypeUtils.typeExp(StandardNames.DETERMINES, parseArgTypes(Abstract.binaryRhs(Abstract
              .binaryRhs(tp)), cxt, errors, varHandler));

      if (isFallback) {
        for (IType argType : argTypes)
          if (!TypeUtils.isTypeVar(argType)) {
            errors.reportError("fallback implementation must be generic", tp.getLoc());
            break;
          }
      }

      argTypes.add(dependent);
      return TypeUtils.typeExp(TypeContracts.contractImplTypeName(Abstract.getId(Abstract.binaryLhs(tp))), argTypes);
    } else if (Abstract.isBinary(tp, StandardNames.OVER)) {
      List<IType> argTypes = parseArgTypes(Abstract.binaryRhs(tp), cxt, errors, varHandler);

      if (isFallback) {
        for (IType argType : argTypes)
          if (!TypeUtils.isTypeVar(argType)
                  && (!(argType instanceof TypeExp) || TypeUtils.isTypeVar(((TypeExp) argType).getTypeCon()))) {
            errors.reportWarning("default implementation should be generic", tp.getLoc());
            break;
          }
      }
      return TypeUtils.typeExp(TypeContracts.contractImplTypeName(Abstract.getId(Abstract.binaryLhs(tp))), argTypes);
    } else {
      errors.reportError("not a valid contract implementation: " + tp, tp.getLoc());
      return StandardTypes.voidType;
    }
  }

  private static void parseAlgebraicConstructors(IAbstract tp, IType type, IAlgebraicType desc,
                                                 Dictionary cxt, Dictionary outer, ErrorReport errors, Map<String,
          TypeVar> typeVars){
    for (IAbstract con : CompilerUtils.unWrap(tp, StandardNames.OR)) {
      if (CompilerUtils.isPrivate(con)) {
        con = CompilerUtils.privateTerm(con);
      }
      if (CompilerUtils.isBraceTerm(con))
        parseRecordConstructor(con, type, desc, cxt, errors, typeVars);
      else if (con instanceof Name)
        parsePositional0(con, type, desc, cxt, errors);
      else if (con instanceof Apply && ((Apply) con).getOperator() instanceof Name)
        parsePositional(con, type, desc, cxt, outer, errors, typeVars);
      else
        errors.reportError("invalid element of algebraic type definition: " + con, con.getLoc());
    }
  }

  private static void parsePositional(IAbstract tp, IType type, IAlgebraicType desc, Dictionary dict, Dictionary outer,
                                      ErrorReport errors, Map<String, TypeVar> typeVars){
    Apply apply = (Apply) tp;
    String label = apply.getOp();

    Dictionary conDict = dict.fork();
    TypeNameHandler varHandler = new RegularTypeName(conDict, typeVars, AccessMode.readOnly, true, errors);

    List<IType> typeArgs = parseArgTypes(apply.getArgs(), conDict, errors, varHandler);
    IType conType = Refresher.generalize(TypeUtils.constructorType(typeArgs, type), dict);
    Collection<IValueSpecifier> specs = desc.getValueSpecifiers();

    final ConstructorSpecifier cons = new ConstructorSpecifier(tp.getLoc(), label, specs.size(), conType, null);

    if (dict.isLocallyDeclared(label, outer))
      errors.reportError("'" + label + "' already defined at " + dict.getVar(label).getLoc(), tp.getLoc());

    specs.add(cons);
  }

  private static void parsePositional0(IAbstract tp, IType type, IAlgebraicType desc,
                                       Dictionary cxt, ErrorReport errors){
    String label = ((Name) tp).getId();
    IType conType = Refresher.generalize(TypeUtils.constructorType(type));

    Collection<IValueSpecifier> specs = desc.getValueSpecifiers();

    ConstructorSpecifier cons = new ConstructorSpecifier(tp.getLoc(), label, specs.size(), conType, null);
    specs.add(cons);

    if (cxt.isDeclaredVar(label))
      errors.reportError("'" + label + "' already defined at " + cxt.getVar(label).getLoc(), tp.getLoc());
  }

  private static void parseRecordConstructor(IAbstract tp, IType type, IAlgebraicType desc, final Dictionary dict,
                                             final ErrorReport errors, Map<String, TypeVar> typeVars){
    final String conName = Abstract.getId(CompilerUtils.braceLabel(tp));
    Dictionary conDict = dict.fork();

    TypeNameHandler varHandler = new RegularTypeName(conDict, typeVars, AccessMode.readOnly, true, errors);
    IType face = parseInterfaceType(tp.getLoc(), CompilerUtils.braceArg(tp), errors, conDict, varHandler);

    IType conType = Freshen.generalizeType(TypeUtils.constructorType(face, type), dict);

    Collection<IValueSpecifier> valueSpecifiers = desc.getValueSpecifiers();
    RecordSpecifier cons = new RecordSpecifier(tp.getLoc(), conName, null, valueSpecifiers.size(), conType);
    valueSpecifiers.add(cons);
  }

  private static IType parseInterfaceType(Location loc, IAbstract tps, ErrorReport errors, final Dictionary dict,
                                          TypeNameHandler varHandler){
    final SortedMap<String, IType> fields = new TreeMap<>();
    final SortedMap<String, IType> types = new TreeMap<>();

    Dictionary rCxt = dict.fork();
    ITypeCollector handler = new TypeCollector(fields, types, errors, rCxt);

    findMemberTypes(loc, tps, handler, rCxt, errors, varHandler);

    TypeInterfaceType face = new TypeInterfaceType(types, fields);
    return Freshen.existentializeType(face, rCxt);
  }

  public static class TypeCollector implements ITypeCollector{
    private final Map<String, IType> elements;
    private final Map<String, IType> exists;
    private final ErrorReport errors;
    private final Dictionary dict;

    public TypeCollector(Map<String, IType> elements, Map<String, IType> types, ErrorReport errors, Dictionary dict){
      this.elements = elements;
      this.exists = types;
      this.errors = errors;
      this.dict = dict;
    }

    @Override
    public void fieldAnnotation(Location loc, String name, IType type){
      elements.put(name, type);
      dict.declareVar(name, new Variable(loc, type, name), AccessMode.readOnly, Visibility.priVate, true);
    }

    @Override
    public void kindAnnotation(Location loc, String name, IType type){
      IType t = exists.get(name);
      if (t == null) {
        exists.put(name, type);
        dict.defineType(new TypeExists(loc, name, type));
      } else {
        assert t instanceof TypeVar;
        try {
          Subsume.subsume(t, type, loc, dict);
        } catch (TypeConstraintException e) {
          errors.reportError(StringUtils.msg("kind of ", name, " already declared to be ", t.kind()));
        }
      }
    }

    @Override
    public void completeInterface(Location loc){
      for (Entry<String, IType> e : exists.entrySet()) {
        if (e.getValue() instanceof TypeVar) {
          TypeVar v = (TypeVar) e.getValue();
          for (ITypeConstraint con : v) {
            if (con instanceof ContractConstraint) {
              ContractConstraint contract = (ContractConstraint) con;
              String instanceName = OverLoader.instanceFunName(contract.getContract());
              IType instanceType = OverLoader.computeDictionaryType(contract.getContract(), loc, AccessMode.readWrite);
              fieldAnnotation(loc, instanceName, instanceType);
            }
          }
        }
      }
    }
  }

  private interface ITypeCollector{
    void fieldAnnotation(Location loc, String name, IType type);

    void kindAnnotation(Location loc, String name, IType type);

    void completeInterface(Location loc);
  }

  private static void findMemberTypes(Location loc, IAbstract types, ITypeCollector collector, Dictionary cxt,
                                      ErrorReport errors, TypeNameHandler varHandler){
    for (IAbstract el : CompilerUtils.unWrap(types)) {
      Location elLoc = el.getLoc();
      if (CompilerUtils.isKindAnnotation(el)) {
        String fieldName = Abstract.getId(CompilerUtils.kindAnnotatedTerm(el));

        IAbstract tpSpec = CompilerUtils.kindAnnotation(el);
        if (Abstract.isIdentifier(tpSpec, StandardNames.TYPE)) {
          TypeVar fieldType = varHandler.newTypeVar(fieldName, elLoc);
          collector.kindAnnotation(elLoc, fieldName, fieldType);
        } else if (Abstract.isBinary(tpSpec, StandardNames.OF)) {
          IAbstract kindArgs = Abstract.deParen(Abstract.binaryRhs(tpSpec));
          int arity = 0;
          if (Abstract.isIdentifier(kindArgs, StandardNames.TYPE))
            arity = 1;
          else if (Abstract.isTupleTerm(kindArgs))
            arity = Abstract.tupleArity(kindArgs);
          else
            errors.reportError("invalid declaration of type: " + el, elLoc);
          collector.kindAnnotation(elLoc, fieldName, TypeVar.var(fieldName, Kind.kind(arity), varHandler.access()));
        } else
          errors.reportError("invalid declaration of member type: " + el, elLoc);

        IAbstract constraint = CompilerUtils.kindAnnotatedConstraint(el);
        if (constraint != null)
          parseConstraints(constraint, cxt, errors, varHandler);
      } else if (CompilerUtils.isTypeEquality(el)) {
        String fieldName = Abstract.getId(CompilerUtils.typeEqualField(el));
        IType tp = parseType(CompilerUtils.typeEqualType(el), cxt, errors, varHandler);
        collector.kindAnnotation(elLoc, fieldName, tp);
      }
    }
    for (IAbstract tp : CompilerUtils.unWrap(types)) {
      if (CompilerUtils.isTypeAnnotation(tp)) {
        String fieldName = Abstract.getId(CompilerUtils.typeAnnotatedTerm(tp));
        IAbstract tpSpec = CompilerUtils.typeAnnotation(tp);
        IType memberType = parseType(tpSpec, cxt, errors, varHandler);
        collector.fieldAnnotation(tpSpec.getLoc(), fieldName, memberType);
      }
    }

    collector.completeInterface(loc);
  }

  public static TypeContract parseTypeContractHead(IAbstract con, Dictionary dict, ErrorReport errors){
    assert CompilerUtils.isContractStmt(con);

    IAbstract tpTerm = CompilerUtils.contractForm(con);

    Map<String, TypeVar> tVars = new HashMap<>();
    TypeNameHandler defHandler = new DefiningTypeName(dict, tVars, AccessMode.readOnly);
    TypeExp conType = parseContractType(tpTerm, dict, errors, defHandler);

    if (conType != null) {
      String contractName = conType.typeLabel();
      String contractImplName = TypeContracts.contractImplTypeName(contractName);
      IType conImplType = TypeUtils.typeExp(contractImplName, conType.getTypeArgs());

      Location loc = con.getLoc();
      TypeDescription contractType = new TypeDescription(loc, Refresher.generalize(conImplType));

      return new TypeContract(loc, contractName, contractType);
    }
    return null;
  }

  public static TypeContract parseTypeContract(IAbstract con, Dictionary dict, ErrorReport errors,
                                               Map<String, Pair<IAbstract, IType>> defaultFuns, Map<String,
          IAbstract> integrity){
    assert CompilerUtils.isContractStmt(con);

    IAbstract tpTerm = CompilerUtils.contractForm(con);
    IAbstract specTerm = CompilerUtils.contractSpec(con);

    Map<String, TypeVar> tVars = new HashMap<>();
    TypeNameHandler varHandler = new RegularTypeName(dict, tVars, AccessMode.readOnly, true, errors);
    TypeNameHandler defHandler = new DefiningTypeName(dict, tVars, AccessMode.readOnly);
    TypeExp conType = parseContractType(tpTerm, dict, errors, defHandler);

    if (conType != null) {
      String contractName = conType.typeLabel();
      String contractImplName = TypeContracts.contractImplTypeName(contractName);
      IType conImplType = TypeUtils.typeExp(contractImplName, conType.getTypeArgs());

      IType face = parseInterfaceType(con.getLoc(), specTerm, errors, dict, varHandler);

      Location loc = con.getLoc();
      RecordSpecifier contractRecord = new RecordSpecifier(loc, contractName, null, 0, Refresher.generalize(TypeUtils
              .constructorType(face, conImplType)));
      TypeDescription contractType = new TypeDescription(loc, Refresher.generalize(conImplType), contractRecord);

      parseDefaults(CompilerUtils.braceTerm(loc, new Name(loc, contractImplName), specTerm), conImplType, dict,
              contractType, defaultFuns, integrity, errors);

      return new TypeContract(loc, contractName, contractType);
    }
    return null;
  }

  public static void fleshoutTypeContract(IAbstract con, TypeContract contract, Dictionary dict, ErrorReport errors,
                                          Map<String, Pair<IAbstract, IType>> defaultFuns, Map<String,
          IAbstract> integrity){
    assert CompilerUtils.isContractStmt(con);

    IAbstract tpTerm = CompilerUtils.contractForm(con);
    IAbstract specTerm = CompilerUtils.contractSpec(con);

    Map<String, TypeVar> tVars = new HashMap<>();
    TypeNameHandler varHandler = new RegularTypeName(dict, tVars, AccessMode.readOnly, true, errors);
    TypeNameHandler defHandler = new DefiningTypeName(dict, tVars, AccessMode.readOnly);
    TypeExp conType = parseContractType(tpTerm, dict, errors, defHandler);

    if (conType != null) {
      String contractName = conType.typeLabel();
      String contractImplName = TypeContracts.contractImplTypeName(contractName);
      IType conImplType = TypeUtils.typeExp(contractImplName, conType.getTypeArgs());

      IType face = parseInterfaceType(con.getLoc(), specTerm, errors, dict, varHandler);

      Location loc = con.getLoc();
      RecordSpecifier contractRecord = new RecordSpecifier(loc, contractName, null, 0, Refresher.generalize(TypeUtils
              .constructorType(face, conImplType)));
      TypeDescription contractType = (TypeDescription) contract.getContractType();
      contractType.defineValueSpecifier(contractImplName, contractRecord);

      parseDefaults(CompilerUtils.braceTerm(loc, new Name(loc, contractImplName), specTerm), conImplType, dict,
              contractType, defaultFuns, integrity, errors);
    }
  }

  public static TypeAlias parseTypeAlias(IAbstract stmt, Dictionary cxt, ErrorReport errors){
    assert CompilerUtils.isTypeAlias(stmt);

    Dictionary tmpCxt = cxt.fork();

    LayeredMap<String, TypeVar> typeVars = new LayeredHash<>();
    TypeNameHandler varHandler = new RegularTypeName(cxt, typeVars, AccessMode.readOnly, true, errors);

    IType thisType = typeHead(CompilerUtils.typeAliasType(stmt), tmpCxt, errors, varHandler);

    IType replacement = parseType(CompilerUtils.typeAliasAlias(stmt), tmpCxt, errors, varHandler);
    return new TypeAlias(stmt.getLoc(), Freshen.generalizeType(TypeUtils.typeExp(StandardNames.ALIAS, thisType,
            replacement), cxt));
  }

  public static void parseDefaults(IAbstract spec, IType thisType, Dictionary cxt, IAlgebraicType desc,
                                   Map<String, Pair<IAbstract, IType>> defaultFuns, Map<String, IAbstract> integrity,
                                   ErrorReport errors){
    for (IAbstract con : CompilerUtils.unWrap(spec, StandardNames.OR)) {
      if (CompilerUtils.isBraceTerm(con)) {
        Location loc = con.getLoc();
        final String conName = Abstract.getId(CompilerUtils.braceLabel(con));
        String typeLabel = thisType.typeLabel();
        RecordSpecifier cons = (RecordSpecifier) desc.getValueSpecifier(conName);
        IType conType = Freshen.freshenForUse(cons.getConType());
        try {
          Subsume.same(TypeUtils.getConstructorResultType(conType), thisType, loc, cxt);
        } catch (TypeConstraintException e) {
          assert false : "should never happen";
        }

        Map<String, Integer> memberIndex = cons.getIndex();
        Map<String, IAbstract> defaults = new HashMap<>();

        locateDefaults(CompilerUtils.braceArg(con), memberIndex.keySet(), defaults, errors);
        locateIntegrityFuns(CompilerUtils.braceArg(con), memberIndex, integrity, CompilerUtils.integrityLabel(
                typeLabel, conName), TypeUtils.getConstructorArgType(conType));

        // Each default becomes a function from the non-default values to the
        // default value

        // Keep track of non-default variables
        List<String> nonDefaults = new ArrayList<>();
        for (Entry<String, Integer> entry : memberIndex.entrySet())
          if (!defaults.containsKey(entry.getKey()))
            nonDefaults.add(entry.getKey());

        IType conArgType = TypeUtils.getConstructorArgType(conType);
        TypeInterface conFace = (TypeInterface) TypeUtils.unwrap(conArgType);

        // Build the special pattern for this record
        String argPtns[] = nonDefaults.toArray(new String[nonDefaults.size()]);
        IType argTypes[] = new IType[argPtns.length];
        for (int ix = 0; ix < argPtns.length; ix++)
          argTypes[ix] = conFace.getFieldType(argPtns[ix]);

        for (Entry<String, IAbstract> entry : defaults.entrySet()) {
          final String member = entry.getKey();
          String defName = CompilerUtils.defaultLabel(typeLabel, conName, member);

          IAbstract args[] = new IAbstract[argPtns.length];
          for (int ix = 0; ix < args.length; ix++)
            args[ix] = DefFinder.isFound(nonDefaults, entry.getValue()) ? CompilerUtils.varPtn(new Name(loc,
                    argPtns[ix])) : CafeSyntax.anonymous(loc);

          // Con#mem(F1,..,Fn) is <deflt>
          IAbstract defFun = Abstract.binary(loc, StandardNames.IS, new Apply(loc, defName, args), entry.getValue());
          defaultFuns.put(defName, Pair.pair(defFun, Refresher.generalize(TypeUtils.functionType(argTypes, conFace
                  .getFieldType(member)))));
        }
      }
    }
  }

  static void locateDefaults(IAbstract content, Collection<String> members, Map<String, IAbstract> defaults,
                             ErrorReport errors){
    for (IAbstract el : CompilerUtils.unWrap(content)) {
      Location loc = el.getLoc();
      if (Abstract.isBinary(el, StandardNames.IS) && Abstract.isUnary(Abstract.binaryLhs(el), StandardNames.DEFAULT)) {
        IAbstract def = Abstract.unaryArg(Abstract.binaryLhs(el));
        def = Abstract.deParen(def);
        if (CompilerUtils.isIdentifier(def)) {
          String att = Abstract.getId(def);
          if (members.contains(att))
            defaults.put(att, Abstract.binaryRhs(el));
          else
            errors.reportError("no such member: " + att, loc);
        } else if (def instanceof Apply) {
          IAbstract op = ((Apply) def).getOperator();
          if (CompilerUtils.isIdentifier(op)) {
            String att = Abstract.getId(op);
            if (members.contains(att))
              defaults.put(att, Abstract.binary(loc, StandardNames.IS, new Apply(loc, StandardNames.FUN_LAMBDA,
                      ((Apply) def).getArgs()), Abstract.binaryRhs(el)));
            else
              errors.reportError("no such member: " + att, loc);
          }
        } else
          errors.reportError("invalid declaration declaration of member type: " + el, loc);
      } else if (Abstract.isBinary(el, StandardNames.ASSIGN)
              && Abstract.isUnary(Abstract.binaryLhs(el), StandardNames.DEFAULT)) {
        IAbstract def = Abstract.unaryArg(Abstract.binaryLhs(el));
        def = Abstract.deParen(def);
        if (CompilerUtils.isIdentifier(def)) {
          String att = Abstract.getId(def);
          if (members.contains(att))
            defaults.put(att, Abstract.unary(el.getLoc(), Cell.label, Abstract.binaryRhs(el)));
          else
            errors.reportError("no such member: " + att, loc);
        } else
          errors.reportError("invalid declaration declaration of default: " + el, loc);
      }
    }
  }

  private static void locateIntegrityFuns(IAbstract content, Map<String, Integer> memberIndex,
                                          Map<String, IAbstract> integrity, final String conName, IType type){
    Wrapper<IAbstract> ass = Wrapper.create(null);

    for (IAbstract el : CompilerUtils.unWrap(content)) {
      if (CompilerUtils.isAssert(el))
        CompilerUtils.extendCondition(ass, CompilerUtils.asserted(el));
    }
    if (!CompilerUtils.isTrivial(ass.get())) {
      Location loc = content.getLoc();
      IAbstract recArg = new Name(loc, GenSym.genSym("__"));
      List<IAbstract> args = new ArrayList<>();
      args.add(recArg);
      List<IAbstract> els = new ArrayList<>();
      TypeInterface face = (TypeInterface) TypeUtils.deRef(type);

      for (String nm : memberIndex.keySet()) {
        IAbstract name = new Name(loc, nm);
        IAbstract fieldExp = CompilerUtils.fieldExp(loc, recArg, name);

        IType elType = face.getFieldType(nm);

        if (TypeUtils.isReferenceType(elType))
          fieldExp = CompilerUtils.shriekTerm(loc, fieldExp);

        IAbstract nmDef = CompilerUtils.isStatement(loc, name, fieldExp);
        els.add(nmDef);
      }
      els.add(CompilerUtils.assertion(loc, ass.get()));
      IAbstract test = CompilerUtils.blockTerm(loc, els);
      IAbstract assertion = CompilerUtils.actionRule(loc, conName, args, test);

      integrity.put(conName, assertion);
    }
  }

  private static class DefFinder extends DefaultAbstractVisitor{
    private final List<String> refs;
    private boolean found = false;

    public DefFinder(List<String> refs){
      this.refs = refs;
    }

    public static boolean isFound(List<String> refs, IAbstract trm){
      DefFinder finder = new DefFinder(refs);
      trm.accept(finder);
      return finder.found;
    }

    @Override
    public void visitName(Name name){
      if (!found && refs.contains(name.getId()))
        found = true;
    }
  }

  // Either a single type or a tuple of types
  private static List<IType> parseArgTypes(IAbstract tp, Dictionary cxt, ErrorReport errors,
                                           TypeNameHandler varHandler){
    List<IType> argTypes = new ArrayList<>();
    if (Abstract.isTupleTerm(tp)) {
      IArray args = ((Apply) tp).getArgs();
      if (!args.isEmpty())
        for (IValue a : args)
          argTypes.add(parseType((IAbstract) a, cxt, errors, varHandler));
      else
        argTypes.add(StandardTypes.unitType);
    } else
      argTypes.add(parseType(tp, cxt, errors, varHandler));
    return argTypes;
  }

  public static ITypeDescription declareType(Dictionary tmpCxt, Dictionary cxt, IAbstract tp, ErrorReport errors){
    Location loc = tp.getLoc();

    LayeredMap<String, TypeVar> typeVars = new LayeredHash<>();
    TypeNameHandler varHandler = new RegularTypeName(cxt, typeVars, AccessMode.readWrite, false, errors);
    IType type = typeHead(CompilerUtils.typeDefnType(tp), tmpCxt, errors, varHandler);

    if (type != null) {
      String name = type.typeLabel();
      if (cxt.getTypeDescription(name) != null)
        errors.reportWarning("type `" + type + "' already declared at " + cxt.getTypeDescription(name).getLoc(), loc);

      TypeDescription desc = new TypeDescription(loc, Refresher.generalize(type, typeVars));
      cxt.defineType(desc);
      return desc;
    } else {
      errors.reportError("bad type definition statement", loc);
      return null;
    }
  }

  private static IType typeHead(IAbstract tp, Dictionary cxt, ErrorReport errors, TypeNameHandler varHandler){
    tp = Abstract.deParen(tp);
    if (tp instanceof Name)
      return TypeUtils.typeExp(Abstract.getId(tp));
    else if (Abstract.isParenTerm(tp))
      return typeHead(Abstract.deParen(tp), cxt, errors, varHandler);
    else if (Abstract.isBinary(tp, StandardNames.WHERE)) {
      IType head = typeHead(Abstract.binaryLhs(tp), cxt, errors, varHandler);
      parseConstraints(Abstract.binaryRhs(tp), cxt, errors, varHandler);
      return head;
    } else if (Abstract.isBinary(tp, StandardNames.OF) && Abstract.isIdentifier(Abstract.binaryLhs(tp))) {
      List<IType> argTypes = new ArrayList<>();
      IAbstract headArgs = Abstract.binaryRhs(tp);

      if (Abstract.isTupleTerm(headArgs)) {
        for (IValue a : ((Apply) headArgs).getArgs())
          argTypes.add(headArg((IAbstract) a, errors, varHandler));
      } else
        argTypes.add(headArg(headArgs, errors, varHandler));

      return TypeUtils.typeExp(Abstract.getId(Abstract.binaryLhs(tp)), argTypes);
    } else {
      errors.reportError("invalid type spec: " + tp, tp.getLoc());
      return null;
    }
  }

  private static IType headArg(IAbstract arg, ErrorReport errors, TypeNameHandler varHandler){
    Location loc = arg.getLoc();

    if (CompilerUtils.isTypeVar(arg)) {
      String tvName = CompilerUtils.typeVarName(arg);
      return varHandler.newTypeVar(tvName, loc);
    } else if (CompilerUtils.isTypeFunVar(arg)) {
      String name = CompilerUtils.typeFunVarName(arg);
      return varHandler.newTypeVar(name, loc);
    } else if (Abstract.isIdentifier(arg))
      return varHandler.newTypeVar(Abstract.getId(arg), loc);
    else {
      errors.reportError("expecting a type variable, not: " + arg, loc);
      return new TypeVar();
    }
  }

  private static List<IType> parseArgTypes(IArray argTuple, Dictionary cxt, ErrorReport errors,
                                           TypeNameHandler varHandler){
    List<IType> types = new ArrayList<>();

    for (IValue a : argTuple)
      types.add(parseType((IAbstract) a, cxt, errors, varHandler));

    return types;
  }

  private static IType typeAlias(Dictionary cxt, IType type, Location loc) throws TypeConstraintException{
    type = TypeUtils.deRef(type);

    final String name = type.typeLabel();

    ITypeDescription typeSpec = cxt.getTypeDescription(name);
    if (typeSpec instanceof ITypeAlias) {
      ITypeAlias alias = (ITypeAlias) typeSpec;
      return alias.apply(type, loc, cxt);
    } else if (typeSpec instanceof TypeExists)
      return type;
    else if (type.kind().equals(Kind.type) && typeSpec != null) {
      Subsume.subsume(type, Freshen.freshenForUse(typeSpec.getType()), loc, cxt, true);
      return type;
    } else
      return type;
  }
}
